(* ---------------------------------------------------------------------------- *)
section ‹Introduction›
(* ---------------------------------------------------------------------------- *)

text ‹The complex plane or some of its parts (e.g., the unit disc or the upper half plane) are often
taken as the domain in which models of various geometries (both Euclidean and non-Euclidean ones)
are formalized. The complex plane gives simpler and more compact formulas than the Cartesian plane.
Within complex plane is easier to describe geometric objects and perform the calculations (usually
shedding some new light on the subject). We give a formalization of the extended complex
plane (given both as a complex projective space and as the Riemann sphere), its objects (points,
circles and lines), and its transformations (Möbius transformations).›

(* ---------------------------------------------------------------------------- *)
section ‹Related work›
(* ---------------------------------------------------------------------------- *)

text‹During the last decade, there have been many results in formalizing
geometry in proof-assistants. Parts of Hilbert’s seminal book
,,Foundations of Geometry'' \cite{hilbert} have been formalized both
in Coq and Isabelle/Isar.  Formalization of first two groups of axioms
in Coq, in an intuitionistic setting was done by Dehlinger et
al. \cite{hilbert-coq}. First formalization in Isabelle/HOL was done
by Fleuriot and Meikele \cite{hilbert-isabelle}, and some further
developments were made in master thesis of Scott \cite{hilbert-scott}.
Large fragments of Tarski's geometry \cite{tarski} have been
formalized in Coq by Narboux et al. \cite{narboux-tarski}. Within Coq,
there are also formalizations of von Plato’s constructive geometry by
Kahn \cite{vonPlato,von-plato-formalization}, French high school
geometry by Guilhot \cite{guilhot} and ruler and compass geometry by
Duprat \cite{duprat2008}, etc.

In our previous work \cite{petrovic2012formalizing}, we have already
formally investigated a Cartesian model of Euclidean geometry. 
›

(* ---------------------------------------------------------------------------- *)
section ‹Background theories› 
(* ---------------------------------------------------------------------------- *)

text ‹In this section we introduce some basic mathematical notions and prove some lemmas needed in the rest of our
formalization. We describe:

    ▪ trigonometric functions,

    ▪ complex numbers, 

    ▪ systems of two and three linear equations with two unknowns (over arbitrary fields), 

    ▪ quadratic equations (over real and complex numbers), systems of quadratic and real
      equations, and systems of two quadratic equations,

    ▪ two-dimensional vectors and matrices over complex numbers.
›

(* -------------------------------------------------------------------------- *)
subsection ‹Library Additions for Trigonometric Functions›
(* -------------------------------------------------------------------------- *)

theory More_Transcendental
  imports Complex_Main "HOL-Library.Periodic_Fun"
begin

text ‹Additional properties of @{term sin} and @{term cos} functions that are later used in proving
conjectures for argument of complex number.›

text ‹Sign of trigonometric functions on some characteristic intervals.›

lemma cos_lt_zero_on_pi2_pi [simp]:
  assumes "x > pi/2" and "x ≤ pi"
  shows "cos x < 0"
  using cos_gt_zero_pi[of "pi - x"] assms
  by simp

text ‹Value of trigonometric functions in points $k\pi$ and $\frac{\pi}{2} + k\pi$.›

lemma sin_kpi [simp]:
  fixes k::int
  shows "sin (k * pi) = 0"
  by (simp add: sin_zero_iff_int2)

lemma cos_odd_kpi [simp]:
  fixes k::int
  assumes "odd k"
  shows "cos (k * pi) = -1"
  by (simp add: assms mult.commute)

lemma cos_even_kpi [simp]:
  fixes k::int
  assumes "even k"
  shows "cos (k * pi) = 1"
  by (simp add: assms mult.commute)

lemma sin_pi2_plus_odd_kpi [simp]:
  fixes k::int
  assumes "odd k"
  shows "sin (pi / 2 + k * pi) = -1"
  using assms
  by (simp add: sin_add)

lemma sin_pi2_plus_even_kpi [simp]:
  fixes k::int
  assumes "even k"
  shows "sin (pi / 2 + k * pi) = 1"
  using assms
  by (simp add: sin_add)

text ‹Solving trigonometric equations and systems with special values (0, 1, or -1) of sine and cosine functions›

lemma cos_0_iff_canon:
  assumes "cos φ = 0" and "-pi < φ" and "φ ≤ pi"
  shows "φ = pi/2 ∨ φ = -pi/2"
  by (smt (verit, best) arccos_0 arccos_cos assms cos_minus divide_minus_left)

lemma sin_0_iff_canon:
  assumes "sin φ = 0" and "-pi < φ" and "φ ≤ pi"
  shows "φ = 0 ∨ φ = pi"
  using assms sin_eq_0_pi by force

lemma cos0_sin1:
  assumes "sin φ = 1"
  shows "∃ k::int. φ = pi/2 + 2*k*pi"
  by (smt (verit, ccfv_threshold) assms cos_diff cos_one_2pi_int cos_pi_half mult_cancel_right1 sin_pi_half sin_plus_pi)

(* TODO: add lemmas for cos = -1, sin = 0 and cos = 0, sin = -1 *)


text ‹Sine is injective on $[-\frac{\pi}{2}, \frac{\pi}{2}]$›

lemma sin_inj:
  assumes "-pi/2 ≤ α ∧ α ≤ pi/2" and "-pi/2 ≤ α' ∧ α' ≤ pi/2"
  assumes "α ≠ α'"
  shows "sin α ≠ sin α'"
  by (metis assms divide_minus_left sin_inj_pi)

text ‹Periodicity of trigonometric functions›

text ‹The following are available in HOL-Decision\_Procs.Approximation\_Bounds, but we want to avoid
that dependency›

lemma sin_periodic_nat [simp]: 
  fixes n :: nat
  shows "sin (x + n * (2 * pi)) = sin x"
  by (metis (no_types, hide_lams) add.commute add.left_neutral cos_2npi cos_one_2pi_int mult.assoc mult.commute mult.left_neutral mult_zero_left sin_add sin_int_2pin)

lemma sin_periodic_int [simp]:
  fixes i :: int
  shows "sin (x + i * (2 * pi)) = sin x"
  by (metis add.right_neutral cos_int_2pin mult.commute mult.right_neutral mult_zero_right sin_add sin_int_2pin)

lemma cos_periodic_nat [simp]: 
  fixes n :: nat
  shows "cos (x + n * (2 * pi)) = cos x"
  by (metis add.left_neutral cos_2npi cos_add cos_periodic mult.assoc mult_2 mult_2_right of_nat_numeral sin_periodic sin_periodic_nat)

lemma cos_periodic_int [simp]:
  fixes i :: int
  shows "cos (x + i * (2 * pi)) = cos x"
  by (metis cos_add cos_int_2pin diff_zero mult.commute mult.right_neutral mult_zero_right sin_int_2pin)

text ‹Values of both sine and cosine are repeated only after multiples of $2\cdot \pi$›

lemma sin_cos_eq:
  fixes a b :: real
  assumes "cos a = cos b" and "sin a = sin b"
  shows "∃ k::int. a - b = 2*k*pi"
  by (metis assms cos_diff cos_one_2pi_int mult.commute sin_cos_squared_add3)

text ‹The following two lemmas are consequences of surjectivity of cosine for the range $[-1, 1]$.›

lemma ex_cos_eq:
  assumes "-pi/2 ≤ α ∧ α ≤ pi/2"
  assumes "a ≥ 0" and "a < 1"
  shows "∃ α'. -pi/2 ≤ α' ∧ α' ≤ pi/2 ∧ α' ≠ α ∧ cos (α - α') = a"
proof-
  have "arccos a > 0" "arccos a ≤ pi/2"
    using ‹a ≥ 0› ‹a < 1›
    using arccos_lt_bounded arccos_le_pi2
    by auto

  show ?thesis
  proof (cases "α - arccos a ≥ - pi/2")
    case True
    thus ?thesis
      using assms ‹arccos a > 0› ‹arccos a ≤ pi/2›
      by (rule_tac x = "α - arccos a" in exI) auto
  next
    case False
    thus ?thesis
      using assms ‹arccos a > 0› ‹arccos a ≤ pi/2›
      by (rule_tac x = "α + arccos a" in exI) auto
  qed
qed

lemma ex_cos_gt:
  assumes "-pi/2 ≤ α ∧ α ≤ pi/2"
  assumes "a < 1"
  shows "∃ α'. -pi/2 ≤ α' ∧ α' ≤ pi/2 ∧ α' ≠ α ∧ cos (α - α') > a"
proof-
  obtain a' where "a' ≥ 0" "a' > a" "a' < 1"
    by (metis assms(2) dense_le_bounded linear not_one_le_zero)
  thus ?thesis
    using ex_cos_eq[of α a'] assms
    by auto
qed

text ‹The function @{term atan2} is a generalization of @{term arctan} that takes a pair of coordinates
of non-zero points returns its angle in the range $[-\pi, \pi)$.›

definition atan2 where
  "atan2 y x =
    (if x > 0 then arctan (y/x)
     else if x < 0 then
          if y > 0 then arctan (y/x) + pi else arctan (y/x) - pi
     else
          if y > 0 then pi/2 else if y < 0 then -pi/2 else 0)"

lemma atan2_bounded: 
  shows "-pi ≤ atan2 y x ∧ atan2 y x < pi"
  using arctan_bounded[of "y/x"] zero_le_arctan_iff[of "y/x"] arctan_le_zero_iff[of "y/x"] zero_less_arctan_iff[of "y/x"] arctan_less_zero_iff[of "y/x"]
  using divide_neg_neg[of y x] divide_neg_pos[of y x] divide_pos_pos[of y x]  divide_pos_neg[of y x]
  unfolding atan2_def
  by (simp (no_asm_simp)) auto

end

(* -------------------------------------------------------------------------- *)
subsection ‹Canonical angle› 
(* -------------------------------------------------------------------------- *)

text ‹Canonize any angle to $(-\pi, \pi]$ (taking account of $2\pi$ periodicity of @{term sin} and
@{term cos}). With this function, for example, multiplicative properties of @{term arg} for complex
numbers can easily be expressed and proved.›

theory Canonical_Angle
imports More_Transcendental
begin


abbreviation canon_ang_P where
 "canon_ang_P α α' ≡ (-pi < α' ∧ α' ≤ pi) ∧ (∃ k::int. α - α' = 2*k*pi)"

definition canon_ang :: "real ⇒ real" ("⇂_⇃") where
  "⇂α⇃ = (THE α'. canon_ang_P α α')"

text ‹There is a canonical angle for every angle.›
lemma canon_ang_ex:
  shows "∃ α'. canon_ang_P α α'"
proof-
  have ***: "∀ α::real. ∃ α'. 0 < α' ∧ α' ≤ 1 ∧ (∃ k::int. α' = α - k)"
  proof
    fix α::real
    show "∃α'>0. α' ≤ 1 ∧ (∃k::int. α' = α - k)"
    proof (cases "α = floor α")
      case True
      thus ?thesis
        by (rule_tac x="α - floor α + 1" in exI, auto) (rule_tac x="floor α - 1" in exI, auto)
    next
      case False
      thus ?thesis
        using real_of_int_floor_ge_diff_one[of "α"]
        using of_int_floor_le[of "α"]
        by (rule_tac x="α - floor α" in exI) smt
    qed
  qed

  have **: "∀ α::real. ∃ α'. 0 < α' ∧ α' ≤ 2 ∧ (∃ k::int. α - α' = 2*k - 1)"
  proof
    fix α::real
    from ***[rule_format, of "(α + 1) /2"]
    obtain α' and k::int where "0 < α'" "α' ≤ 1" "α' = (α + 1)/2 - k"
      by force
    hence "0 < α'" "α' ≤ 1" "α' = α/2 - k + 1/2"
      by auto
    thus "∃α'>0. α' ≤ 2 ∧ (∃k::int. α - α' = real_of_int (2 * k - 1))"
      by (rule_tac x="2*α'" in exI) auto
  qed
  have *: "∀ α::real. ∃ α'. -1 < α' ∧ α' ≤ 1 ∧ (∃ k::int. α - α' = 2*k)"
  proof
    fix α::real
    from ** obtain α' and k :: int where
      "0 < α' ∧ α' ≤ 2 ∧ α - α' = 2*k - 1"
      by force
    thus "∃α'>-1. α' ≤ 1 ∧ (∃k. α - α' = real_of_int (2 * (k::int)))"
      by (rule_tac x="α' - 1" in exI) (auto simp add: field_simps)
  qed
  obtain α' k where 1: "α' >- 1 ∧ α' ≤ 1" and 2: "α / pi - α' = real_of_int (2 * k)"
    using *[rule_format, of "α / pi"]
    by auto
  have "α'*pi > -pi ∧ α'*pi ≤ pi" 
    using 1
    by (smt mult.commute mult_le_cancel_left1 mult_minus_right pi_gt_zero)
  moreover
  have "α - α'*pi = 2 * real_of_int k * pi"
    using 2
    by (auto simp add: field_simps)
  ultimately
  show ?thesis
    by auto
qed

text ‹Canonical angle of any angle is unique.›
lemma canon_ang_unique:
  assumes "canon_ang_P α α⇩1" and "canon_ang_P α α⇩2"
  shows "α⇩1 = α⇩2"
proof-
  obtain k1::int where "α - α⇩1 = 2*k1*pi"
    using assms(1)
    by auto
  obtain k2::int where "α - α⇩2 = 2*k2*pi"
    using assms(2)
    by auto
  hence *: "-α⇩1 + α⇩2 = 2*(k1 - k2)*pi"
    using ‹α - α⇩1 = 2*k1*pi›
    by (simp add:field_simps)
  moreover
  have "-α⇩1 + α⇩2 < 2 * pi" "-α⇩1 + α⇩2 > -2*pi"
    using assms
    by auto
  ultimately
  have "-α⇩1 + α⇩2 = 0"
    using mult_less_cancel_right[of "-2" pi "real_of_int(2 * (k1 - k2))"]
    by auto
  thus ?thesis
    by auto
qed

text ‹Canonical angle is always in $(-\pi, \pi]$ and differs from the starting angle by $2k\pi$.›
lemma canon_ang:
  shows "-pi < ⇂α⇃" and "⇂α⇃ ≤ pi" and "∃ k::int. α - ⇂α⇃ = 2*k*pi"
proof-
  obtain α' where "canon_ang_P α α'"
    using canon_ang_ex[of α]
    by auto
  have "canon_ang_P α ⇂α⇃"
    unfolding canon_ang_def
  proof (rule theI[where a="α'"])
    show "canon_ang_P α α'"
      by fact
  next
    fix α''
    assume "canon_ang_P α α''"
    thus "α'' = α'"
      using ‹canon_ang_P α α'›
      using canon_ang_unique[of α' α α'']
      by simp
  qed
  thus "-pi < ⇂α⇃" "⇂α⇃ ≤ pi" "∃ k::int. α - ⇂α⇃ = 2*k*pi"
    by auto
qed

text ‹Angles in $(-\pi, \pi]$ are already canonical.›
lemma canon_ang_id:
  assumes  "-pi < α ∧ α ≤ pi"
  shows "⇂α⇃ = α"
  using assms
  using canon_ang_unique[of "canon_ang α" α α] canon_ang[of α]
  by auto

text ‹Angles that differ by $2k\pi$ have equal canonical angles.›
lemma canon_ang_eq:
  assumes "∃ k::int. α⇩1 - α⇩2 = 2*k*pi"
  shows "⇂α⇩1⇃ = ⇂α⇩2⇃"
proof-
  obtain k'::int where *: "- pi < ⇂α⇩1⇃" "⇂α⇩1⇃ ≤ pi" "α⇩1 - ⇂α⇩1⇃ = 2 * k' * pi"
    using canon_ang[of α⇩1]
    by auto

  obtain k''::int where **: "- pi < ⇂α⇩2⇃" "⇂α⇩2⇃ ≤ pi" "α⇩2 - ⇂α⇩2⇃ = 2 * k'' * pi"
    using canon_ang[of α⇩2]
    by auto

  obtain k::int where ***: "α⇩1 - α⇩2 = 2*k*pi"
    using assms
    by auto

  have "∃m::int. α⇩1 - ⇂α⇩2⇃ = 2 * m * pi"
    using **(3) ***
    by (rule_tac x="k+k''" in exI) (auto simp add: field_simps)

  thus ?thesis
    using canon_ang_unique[of "⇂α⇩1⇃" α⇩1 "⇂α⇩2⇃"] * **
    by auto
qed

text ‹Introduction and elimination rules›
lemma canon_ang_eqI:
  assumes "∃k::int. α' - α = 2 * k * pi" and "- pi < α' ∧ α' ≤ pi"
  shows "⇂α⇃ = α'"
  using assms
  using canon_ang_eq[of α' α]
  using canon_ang_id[of α']
  by auto

lemma canon_ang_eqE:
  assumes "⇂α⇩1⇃ = ⇂α⇩2⇃"
  shows "∃ (k::int). α⇩1 - α⇩2 = 2 *k * pi"
proof-
  obtain k1 k2 :: int where
    "α⇩1 - ⇂α⇩1⇃ = 2 * k1 * pi"
    "α⇩2 - ⇂α⇩2⇃ = 2 * k2 * pi"
    using canon_ang[of α⇩1] canon_ang[of α⇩2]
    by auto
  thus ?thesis
    using assms
    by (rule_tac x="k1 - k2" in exI) (auto simp add: field_simps)
qed

text ‹Canonical angle of opposite angle›

lemma canon_ang_uminus:
  assumes "⇂α⇃ ≠ pi"
  shows "⇂-α⇃ = -⇂α⇃"
proof (rule canon_ang_eqI)
  show "∃x::int. - ⇂α⇃ - - α = 2 * x * pi"
    using canon_ang(3)[of α]
    by (metis minus_diff_eq minus_diff_minus)
next
  show "- pi < - ⇂α⇃ ∧ - ⇂α⇃ ≤ pi"
    using canon_ang(1)[of α] canon_ang(2)[of α] assms
    by auto
qed

lemma canon_ang_uminus_pi:
  assumes "⇂α⇃ = pi"
  shows "⇂-α⇃ = ⇂α⇃"
proof (rule canon_ang_eqI)
  obtain k::int where "α - ⇂α⇃ = 2 * k * pi"
    using canon_ang(3)[of α]
    by auto
  thus "∃x::int. ⇂α⇃ - - α = 2 * x * pi"
    using assms
    by (rule_tac x="k+(1::int)" in exI) (auto simp add: field_simps)
next
  show "- pi < ⇂α⇃ ∧ ⇂α⇃ ≤ pi"
    using assms
    by auto
qed

text ‹Canonical angle of difference of two angles›
lemma canon_ang_diff:
  shows "⇂α - β⇃ = ⇂⇂α⇃ - ⇂β⇃⇃"
proof (rule canon_ang_eq)
  show "∃x::int. α - β - (⇂α⇃ - ⇂β⇃) = 2 * x * pi"
  proof-
    obtain k1::int where "α - ⇂α⇃ = 2*k1*pi"
      using canon_ang(3)
      by auto
    moreover
    obtain k2::int where "β - ⇂β⇃ = 2*k2*pi"
      using canon_ang(3)
      by auto
    ultimately
    show ?thesis
      by (rule_tac x="k1 - k2" in exI) (auto simp add: field_simps)
  qed
qed

text ‹Canonical angle of sum of two angles›
lemma canon_ang_sum:
  shows "⇂α + β⇃ = ⇂⇂α⇃ + ⇂β⇃⇃"
proof (rule canon_ang_eq)
  show "∃x::int. α + β - (⇂α⇃ + ⇂β⇃) = 2 * x * pi"
  proof-
    obtain k1::int where "α - ⇂α⇃ = 2*k1*pi"
      using canon_ang(3)
      by auto
    moreover
    obtain k2::int where "β - ⇂β⇃ = 2*k2*pi"
      using canon_ang(3)
      by auto
    ultimately
    show ?thesis
      by (rule_tac x="k1 + k2" in exI) (auto simp add: field_simps)
  qed
qed

text ‹Canonical angle of angle from $(0, 2\pi]$ shifted by $\pi$›

lemma canon_ang_plus_pi1:
  assumes "0 < α" and "α ≤ 2*pi"
  shows "⇂α + pi⇃ = α - pi"
proof (rule canon_ang_eqI)
  show "∃ x::int. α - pi - (α + pi) = 2 * x * pi"
    by (rule_tac x="-1" in exI) auto
next
  show "- pi < α - pi ∧ α - pi ≤ pi"
    using assms
    by auto
qed

lemma canon_ang_minus_pi1:
  assumes "0 < α" and "α ≤ 2*pi"
  shows "⇂α - pi⇃ = α - pi"
proof (rule canon_ang_id)
  show "- pi < α - pi ∧ α - pi ≤ pi"
    using assms
    by auto
qed

text ‹Canonical angle of angles from $(-2\pi, 0]$ shifted by $\pi$›

lemma canon_ang_plus_pi2:
  assumes "-2*pi < α" and "α ≤ 0"
  shows "⇂α + pi⇃ = α + pi"
proof (rule canon_ang_id)
  show "- pi < α + pi ∧ α + pi ≤ pi"
    using assms
    by auto
qed

lemma canon_ang_minus_pi2:
  assumes "-2*pi < α" and "α ≤ 0"
  shows "⇂α - pi⇃ = α + pi"
proof (rule canon_ang_eqI)
  show "∃ x::int. α + pi - (α - pi) = 2 * x * pi"
    by (rule_tac x="1" in exI) auto
next
  show "- pi < α + pi ∧ α + pi ≤ pi"
    using assms
    by auto
qed

text ‹Canonical angle of angle in $(\pi, 3\pi]$.›
lemma canon_ang_pi_3pi: 
  assumes "pi < α" and "α ≤ 3 * pi"
  shows "⇂α⇃ = α - 2*pi"
proof-
  have "∃x. - pi = pi * real_of_int x"
    by (rule_tac x="-1" in exI, simp)
  thus ?thesis
    using assms canon_ang_eqI[of "α - 2*pi" "α"]
    by auto
qed

text ‹Canonical angle of angle in $(-3\pi, -\pi]$.›
lemma canon_ang_minus_3pi_minus_pi: 
  assumes "-3*pi < α" and "α ≤ -pi"
  shows "⇂α⇃ = α + 2*pi"
proof-
  have "∃x. pi = pi * real_of_int x"
    by (rule_tac x="1" in exI, simp)
  thus ?thesis
    using assms canon_ang_eqI[of "α + 2*pi" "α"]
    by auto
qed

text ‹Canonical angles for some special angles›

lemma zero_canonical [simp]:
  shows "⇂0⇃ = 0"
  using canon_ang_eqI[of 0 0]
  by simp

lemma pi_canonical [simp]:
  shows "⇂pi⇃ = pi"
  by (simp add: canon_ang_id)

lemma two_pi_canonical [simp]:
  shows "⇂2 * pi⇃ = 0"
  using canon_ang_plus_pi1[of "pi"]
  by simp

text ‹Canonization preserves sine and cosine›
lemma canon_ang_sin [simp]:
  shows "sin ⇂α⇃ = sin α"
proof-
  obtain x::int where "α = ⇂α⇃ + pi * (x * 2)"
    using canon_ang(3)[of α]
    by (auto simp add: field_simps)
  thus ?thesis
    using sin_periodic_int[of "⇂α⇃" x]
    by (simp add: field_simps)
qed

lemma canon_ang_cos [simp]:
  shows "cos ⇂α⇃ = cos α"
proof-
  obtain x::int where "α = ⇂α⇃ + pi * (x * 2)"
    using canon_ang(3)[of α]
    by (auto simp add: field_simps)
  thus ?thesis
    using cos_periodic_int[of "⇂α⇃" x]
    by (simp add: field_simps)
qed

end

(* -------------------------------------------------------------------------- *)
subsection ‹Library Additions for Complex Numbers›
(* -------------------------------------------------------------------------- *)

text ‹Some additional lemmas about complex numbers.›

theory More_Complex
  imports Complex_Main More_Transcendental Canonical_Angle
begin

text ‹Conjugation and @{term cis}›
          
declare cis_cnj[simp] 

lemma rcis_cnj: 
  shows "cnj a = rcis (cmod a) (- arg a)"
  by (subst rcis_cmod_arg[of a, symmetric]) (simp add: rcis_def)

lemmas complex_cnj = complex_cnj_diff complex_cnj_mult complex_cnj_add complex_cnj_divide complex_cnj_minus

text ‹Some properties for @{term complex_of_real}. Also, since it is often used in our
formalization we abbreviate it to @{term cor}.›

abbreviation cor :: "real ⇒ complex" where
  "cor ≡ complex_of_real"

lemma cmod_cis [simp]:
  assumes "a ≠ 0"
  shows "cor (cmod a) * cis (arg a) = a"
  using assms
  by (metis rcis_cmod_arg rcis_def)

lemma cis_cmod [simp]:
  assumes "a ≠ 0"
  shows "cis (arg a) * cor (cmod a) = a"
  using assms cmod_cis[of a]
  by (simp add: field_simps)

lemma cor_squared:
  shows "(cor x)⇧2 = cor (x⇧2)"
  by (simp add: power2_eq_square)

lemma cor_sqrt_mult_cor_sqrt [simp]:
  shows "cor (sqrt A) * cor (sqrt A) = cor ¦A¦"
  by (metis of_real_mult real_sqrt_mult_self)

lemma cor_eq_0: "cor x + 𝗂 * cor y = 0 ⟷ x = 0 ∧ y = 0"
 by (metis Complex_eq Im_complex_of_real Im_i_times Re_complex_of_real add_cancel_left_left of_real_eq_0_iff plus_complex.sel(2) zero_complex.code)

lemma one_plus_square_neq_zero [simp]:
  shows "1 + (cor x)⇧2 ≠ 0"
  by (metis (hide_lams, no_types) of_real_1 of_real_add of_real_eq_0_iff of_real_power power_one sum_power2_eq_zero_iff zero_neq_one)

text ‹Additional lemmas about @{term Complex} constructor. Following newer versions of Isabelle,
these should be deprecated.›

lemma complex_real_two [simp]:
  shows "Complex 2 0 = 2"
  by (simp add: Complex_eq)

lemma complex_double [simp]:
  shows "(Complex a b) * 2 = Complex (2*a) (2*b)"
  by (simp add: Complex_eq)

lemma complex_half [simp]: 
  shows "(Complex a b) / 2 = Complex (a/2) (b/2)"
  by (subst complex_eq_iff) auto

lemma Complex_scale1:
  shows "Complex (a * b) (a * c) = cor a * Complex b c"
  unfolding complex_of_real_def
  unfolding Complex_eq
  by (auto simp add: field_simps)

lemma Complex_scale2: 
  shows "Complex (a * c) (b * c) = Complex a b * cor c"
  unfolding complex_of_real_def
  unfolding Complex_eq
  by (auto simp add: field_simps)

lemma Complex_scale3: 
  shows "Complex (a / b) (a / c) = cor a * Complex (1 / b) (1 / c)"
  unfolding complex_of_real_def
  unfolding Complex_eq
  by (auto simp add: field_simps)

lemma Complex_scale4:
  shows "c ≠ 0 ⟹ Complex (a / c) (b / c) = Complex a b / cor c"
  unfolding complex_of_real_def
  unfolding Complex_eq
  by (auto simp add: field_simps power2_eq_square)

lemma Complex_Re_express_cnj:
  shows "Complex (Re z) 0 = (z + cnj z) / 2"
  by (cases z) (simp add: Complex_eq)

lemma Complex_Im_express_cnj:
  shows "Complex 0 (Im z) = (z - cnj z)/2"
  by (cases z) (simp add: Complex_eq)

text ‹Additional properties of @{term cmod}.›

lemma complex_mult_cnj_cmod:
  shows "z * cnj z = cor ((cmod z)⇧2)"
  using complex_norm_square
  by auto

lemma cmod_square: 
  shows "(cmod z)⇧2 = Re (z * cnj z)"
  using complex_mult_cnj_cmod[of z]
  by (simp add: power2_eq_square)

lemma cor_cmod_power_4 [simp]:
  shows "cor (cmod z) ^ 4 = (z * cnj z)⇧2"
  by (simp add: complex_mult_cnj_cmod)

lemma cnjE:
  assumes "x ≠ 0"
  shows "cnj x = cor ((cmod x)⇧2) / x"
  using complex_mult_cnj_cmod[of x] assms
  by (auto simp add: field_simps)

lemma cmod_cor_divide [simp]:
  shows "cmod (z / cor k) = cmod z / ¦k¦"
  by (simp add: norm_divide)

lemma cmod_mult_minus_left_distrib [simp]:
  shows "cmod (z*z1 - z*z2) = cmod z * cmod(z1 - z2)"
  by (metis norm_mult right_diff_distrib)

lemma cmod_eqI:
  assumes "z1 * cnj z1 = z2 * cnj z2"
  shows "cmod z1 = cmod z2"
  using assms
  by (subst complex_mod_sqrt_Re_mult_cnj)+ auto

lemma cmod_eqE:
  assumes "cmod z1 = cmod z2"
  shows "z1 * cnj z1 = z2 * cnj z2"
  by (simp add: assms complex_mult_cnj_cmod)

lemma cmod_eq_one [simp]:
  shows "cmod a = 1 ⟷ a*cnj a = 1"
  by (metis cmod_eqE cmod_eqI complex_cnj_one monoid_mult_class.mult.left_neutral norm_one)

text ‹We introduce @{term is_real} (the imaginary part of complex number is zero) and @{term is_imag}
(real part of complex number is zero) operators and prove some of their properties.›

abbreviation is_real where
  "is_real z ≡ Im z = 0"

abbreviation is_imag where
  "is_imag z ≡ Re z = 0"

lemma real_imag_0:
  assumes "is_real a" "is_imag a" 
  shows "a = 0"
  using assms
  by (simp add: complex.expand)

lemma complex_eq_if_Re_eq:
  assumes "is_real z1" and "is_real z2"
  shows "z1 = z2 ⟷ Re z1 = Re z2"
  using assms
  by (cases z1, cases z2) auto

lemma mult_reals [simp]:
  assumes "is_real a" and "is_real b"
  shows "is_real (a * b)"
  using assms
  by auto

lemma div_reals [simp]:
  assumes "is_real a" and "is_real b"
  shows "is_real (a / b)"
  using assms
  by (simp add: complex_is_Real_iff)

lemma complex_of_real_Re [simp]:
  assumes "is_real k"
  shows "cor (Re k) = k"
  using assms
  by (cases k) (auto simp add: complex_of_real_def)

lemma cor_cmod_real:
  assumes "is_real a"
  shows "cor (cmod a) = a ∨ cor (cmod a) = -a"
  using assms
  unfolding cmod_def
  by (cases "Re a > 0") auto

lemma eq_cnj_iff_real:
  shows "cnj z = z ⟷ is_real z"
  by (cases z) (simp add: Complex_eq)

lemma eq_minus_cnj_iff_imag:
  shows "cnj z = -z ⟷ is_imag z"
  by (cases z) (simp add: Complex_eq)

lemma Re_divide_real:
  assumes "is_real b" and "b ≠ 0"
  shows "Re (a / b) = (Re a) / (Re b)"
  using assms
  by (simp add: complex_is_Real_iff)

lemma Re_mult_real:
  assumes "is_real a"
  shows "Re (a * b) = (Re a) * (Re b)"
  using assms
  by simp

lemma Im_mult_real:
  assumes "is_real a"
  shows "Im (a * b) = (Re a) * (Im b)"
  using assms
  by simp

lemma Im_divide_real:
  assumes "is_real b" and "b ≠ 0"
  shows "Im (a / b) = (Im a) / (Re b)"
  using assms
  by (simp add: complex_is_Real_iff)

lemma Re_sgn:
  assumes "is_real R"
  shows "Re (sgn R) = sgn (Re R)"
  using assms
  by (metis Re_sgn complex_of_real_Re norm_of_real real_sgn_eq)

lemma is_real_div:
  assumes "b ≠ 0"
  shows "is_real (a / b) ⟷ a*cnj b = b*cnj a"
  using assms
  by (metis complex_cnj_divide complex_cnj_zero_iff eq_cnj_iff_real frac_eq_eq mult.commute)

lemma is_real_mult_real:
  assumes "is_real a" and "a ≠ 0"
  shows "is_real b ⟷ is_real (a * b)"
  using assms
  by (cases a, auto simp add: Complex_eq)

lemma Im_express_cnj:
  shows "Im z = (z - cnj z) / (2 * 𝗂)"
  by (simp add: complex_diff_cnj field_simps)

lemma Re_express_cnj: 
  shows "Re z = (z + cnj z) / 2"
  by (simp add: complex_add_cnj)

text ‹Rotation of complex number for 90 degrees in the positive direction.›

abbreviation rot90 where
  "rot90 z ≡ Complex (-Im z) (Re z)"

lemma rot90_ii: 
  shows "rot90 z = z * 𝗂"
  by (metis Complex_mult_i complex_surj)

text ‹With @{term cnj_mix} we introduce scalar product between complex vectors. This operation shows
to be useful to succinctly express some conditions.›

abbreviation cnj_mix where
  "cnj_mix z1 z2 ≡ cnj z1 * z2 + z1 * cnj z2"

abbreviation scalprod where
  "scalprod z1 z2 ≡ cnj_mix z1 z2 / 2"

lemma cnj_mix_minus:
  shows "cnj z1*z2 - z1*cnj z2 = 𝗂 * cnj_mix (rot90 z1) z2"
  by (cases z1, cases z2) (simp add: Complex_eq field_simps)

lemma cnj_mix_minus':
  shows "cnj z1*z2 - z1*cnj z2 = rot90 (cnj_mix (rot90 z1) z2)"
  by (cases z1, cases z2) (simp add: Complex_eq field_simps)

lemma cnj_mix_real [simp]:
  shows "is_real (cnj_mix z1 z2)"
  by (cases z1, cases z2) simp

lemma scalprod_real [simp]:
  shows "is_real (scalprod z1 z2)"
  using cnj_mix_real
  by simp

text ‹Additional properties of @{term cis} function.›

lemma cis_minus_pi2 [simp]:
  shows "cis (-pi/2) = -𝗂"
  by (simp add: cis_inverse[symmetric])

lemma cis_pi2_minus_x [simp]:
  shows "cis (pi/2 - x) = 𝗂 * cis(-x)"
  using cis_divide[of "pi/2" x, symmetric]
  using cis_divide[of 0 x, symmetric]
  by simp

lemma cis_pm_pi [simp]: 
  shows "cis (x - pi) = - cis x" and  "cis (x + pi) = - cis x"
  by (simp add: cis.ctr complex_minus)+


lemma cis_times_cis_opposite [simp]: 
  shows "cis φ * cis (- φ) = 1"
  by (simp add: cis_mult)

text ‹@{term cis} repeats only after $2k\pi$›
lemma cis_eq:
  assumes "cis a = cis b"
  shows "∃ k::int. a - b = 2 * k * pi"
  using assms sin_cos_eq[of a b]
  using cis.sel[of a] cis.sel[of b]
  by (cases "cis a", cases "cis b") auto

text ‹@{term cis} is injective on $(-\pi, \pi]$.›
lemma cis_inj:
  assumes "-pi < α" and "α ≤ pi" and "-pi < α'" and "α' ≤ pi"
  assumes "cis α = cis α'"
  shows "α = α'"
  using assms
  by (metis arg_unique sgn_cis)

text ‹@{term cis} of an angle combined with @{term cis} of the opposite angle›

lemma cis_diff_cis_opposite [simp]: 
  shows "cis φ - cis (- φ) = 2 * 𝗂 * sin φ"
  using Im_express_cnj[of "cis φ"]
  by simp

lemma cis_opposite_diff_cis [simp]:
  shows "cis (-φ) - cis (φ) = - 2 * 𝗂 * sin φ"
  using cis_diff_cis_opposite[of "-φ"]
  by simp

lemma cis_add_cis_opposite [simp]: 
  shows "cis φ + cis (-φ) = 2 * cos φ"
  by (metis cis.sel(1) cis_cnj complex_add_cnj)

text ‹@{term cis} equal to 1 or -1›
lemma cis_one [simp]:
  assumes "sin φ = 0" and "cos φ = 1"
  shows "cis φ = 1"
  using assms
  by (auto simp add: cis.ctr one_complex.code)

lemma cis_minus_one [simp]:
  assumes "sin φ = 0" and "cos φ = -1"
  shows "cis φ = -1"
  using assms
  by (auto simp add: cis.ctr Complex_eq_neg_1)

(* -------------------------------------------------------------------------- *)
subsubsection ‹Additional properties of complex number argument›
(* -------------------------------------------------------------------------- *)

text ‹@{term arg} of real numbers›

lemma is_real_arg1:
  assumes "arg z = 0 ∨ arg z = pi"
  shows "is_real z"
  using assms
  using rcis_cmod_arg[of z] Im_rcis[of "cmod z" "arg z"]
  by auto

lemma is_real_arg2:
  assumes "is_real z"
  shows "arg z = 0 ∨ arg z = pi"
proof (cases "z = 0")
  case False
  thus ?thesis
    using arg_bounded[of z]
    by (smt (verit, best) Im_sgn assms cis.simps(2) cis_arg div_0 sin_zero_pi_iff)
qed (auto simp add: arg_zero)

lemma arg_complex_of_real_positive [simp]:
  assumes "k > 0"
  shows "arg (cor k) = 0"
proof-
  have "cos (arg (Complex k 0)) > 0"
    using assms
    using rcis_cmod_arg[of "Complex k 0"] Re_rcis[of "cmod (Complex k 0)" "arg (Complex k 0)"]
    using cmod_eq_Re by force
  thus ?thesis
    using assms is_real_arg2[of "cor k"]
    unfolding complex_of_real_def
    by auto
qed

lemma arg_complex_of_real_negative [simp]:
  assumes "k < 0"
  shows "arg (cor k) = pi"
proof-
  have "cos (arg (Complex k 0)) < 0"
    using ‹k < 0› rcis_cmod_arg[of "Complex k 0"] Re_rcis[of "cmod (Complex k 0)" "arg (Complex k 0)"]
    by (metis complex.sel(1) mult_less_0_iff norm_not_less_zero)
  thus ?thesis
    using assms is_real_arg2[of "cor k"]
    unfolding complex_of_real_def
    by auto
qed

lemma arg_0_iff:
  shows "z ≠ 0 ∧ arg z = 0 ⟷ is_real z ∧ Re z > 0"
  by (smt arg_complex_of_real_negative arg_complex_of_real_positive arg_zero complex_of_real_Re is_real_arg1 pi_gt_zero zero_complex.simps)

lemma arg_pi_iff:
  shows "arg z = pi ⟷ is_real z ∧ Re z < 0"
  by (smt arg_complex_of_real_negative arg_complex_of_real_positive arg_zero complex_of_real_Re is_real_arg1 pi_gt_zero zero_complex.simps)


text ‹@{term arg} of imaginary numbers›

lemma is_imag_arg1:
  assumes "arg z = pi/2 ∨ arg z = -pi/2"
  shows "is_imag z"
  using assms
  using rcis_cmod_arg[of z] Re_rcis[of "cmod z" "arg z"]
  by (metis cos_minus cos_pi_half minus_divide_left mult_eq_0_iff)

lemma is_imag_arg2:
  assumes "is_imag z" and "z ≠ 0"
  shows "arg z = pi/2 ∨ arg z = -pi/2"
  using arg_bounded assms cos_0_iff_canon cos_arg_i_mult_zero by presburger

lemma arg_complex_of_real_times_i_positive [simp]:
  assumes "k > 0"
  shows "arg (cor k * 𝗂) = pi / 2"
proof-
  have "sin (arg (Complex 0 k)) > 0"
    using ‹k > 0› rcis_cmod_arg[of "Complex 0 k"] Im_rcis[of "cmod (Complex 0 k)" "arg (Complex 0 k)"]
    by (smt complex.sel(2) mult_nonneg_nonpos norm_ge_zero)
  thus ?thesis
    using assms is_imag_arg2[of "cor k * 𝗂"]
    using arg_zero complex_of_real_i
    by force
qed

lemma arg_complex_of_real_times_i_negative [simp]:
  assumes "k < 0"
  shows "arg (cor k * 𝗂) = - pi / 2"
proof-
  have "sin (arg (Complex 0 k)) < 0"
    using ‹k < 0› rcis_cmod_arg[of "Complex 0 k"] Im_rcis[of "cmod (Complex 0 k)" "arg (Complex 0 k)"]
    by (metis complex.sel(2) mult_less_0_iff norm_not_less_zero)
  thus ?thesis
    using assms is_imag_arg2[of "cor k * 𝗂"]
    using arg_zero complex_of_real_i[of k]
    by (smt complex.sel(1) sin_pi_half sin_zero)
qed

lemma arg_pi2_iff:
  shows "z ≠ 0 ∧ arg z = pi / 2 ⟷ is_imag z ∧ Im z > 0"
  by (smt Im_rcis Re_i_times Re_rcis arcsin_minus_1 cos_pi_half divide_minus_left mult.commute mult_cancel_right1 rcis_cmod_arg is_imag_arg2 sin_arcsin sin_pi_half zero_less_mult_pos zero_less_norm_iff)

lemma arg_minus_pi2_iff:
  shows "z ≠ 0 ∧ arg z = - pi / 2 ⟷ is_imag z ∧ Im z < 0"
  by (smt arg_pi2_iff complex.expand divide_cancel_right pi_neq_zero is_imag_arg1 is_imag_arg2 zero_complex.simps(1) zero_complex.simps(2))

lemma arg_ii [simp]:
  shows "arg 𝗂 = pi/2"
  by (metis arg_pi2_iff imaginary_unit.sel zero_less_one)

lemma arg_minus_ii [simp]: 
  shows "arg (-𝗂) = -pi/2"
proof-
  have "-𝗂 = cis (arg (- 𝗂))"
    using rcis_cmod_arg[of "-𝗂"]
    by (simp add: rcis_def)
  hence "cos (arg (-𝗂)) = 0" "sin (arg (-𝗂)) = -1"
    using cis.simps[of "arg (-𝗂)"]
    by auto
  thus ?thesis
    using cos_0_iff_canon[of "arg (-𝗂)"] arg_bounded[of "-𝗂"]
    by fastforce
qed

text ‹Argument is a canonical angle›

lemma canon_ang_arg:
  shows "⇂arg z⇃ = arg z"
  using canon_ang_id[of "arg z"] arg_bounded
  by simp

lemma arg_cis:
  shows "arg (cis φ) = ⇂φ⇃"
  using arg_unique canon_ang canon_ang_cos canon_ang_sin cis.ctr sgn_cis by presburger

text ‹Cosine and sine of @{term arg}›

lemma cos_arg:
  assumes "z ≠ 0"
  shows "cos (arg z) = Re z / cmod z"
  by (metis Complex.Re_sgn cis.simps(1) assms cis_arg)

lemma sin_arg:
  assumes "z ≠ 0"
  shows "sin (arg z) = Im z / cmod z"
  by (metis Complex.Im_sgn cis.simps(2) assms cis_arg)

text ‹Argument of product›

lemma cis_arg_mult:
  assumes "z1 * z2 ≠ 0"
  shows "cis (arg (z1 * z2)) = cis (arg z1 + arg z2)"
  by (metis assms cis_arg cis_mult mult_eq_0_iff sgn_mult)

lemma arg_mult_2kpi:
  assumes "z1 * z2 ≠ 0"
  shows "∃ k::int. arg (z1 * z2) = arg z1 + arg z2 + 2*k*pi"
proof-
  have "cis (arg (z1*z2)) = cis (arg z1 + arg z2)"
    by (rule cis_arg_mult[OF assms])
  thus ?thesis
    using cis_eq[of "arg (z1*z2)" "arg z1 + arg z2"]
    by (auto simp add: field_simps)
qed

lemma arg_mult:
  assumes "z1 * z2 ≠ 0"
  shows "arg(z1 * z2) = ⇂arg z1 + arg z2⇃"
proof-
  obtain k::int where "arg(z1 * z2) = arg z1 + arg z2 + 2*k*pi"
    using arg_mult_2kpi[of z1 z2]
    using assms
    by auto
  hence "⇂arg(z1 * z2)⇃ = ⇂arg z1 + arg z2⇃"
    using canon_ang_eq
    by(simp add:field_simps)
  thus ?thesis
    using canon_ang_arg[of "z1*z2"]
    by auto
qed

lemma arg_mult_real_positive [simp]:
  assumes "k > 0"
  shows "arg (cor k * z) = arg z"
proof (cases "z = 0")
  case False
  thus ?thesis
    using arg_mult assms canon_ang_arg by force
qed (auto simp: arg_zero)

lemma arg_mult_real_negative [simp]:
  assumes "k < 0"
  shows "arg (cor k * z) = arg (-z)"
proof (cases "z = 0")
  case False
  thus ?thesis
    using assms
    by (metis arg_mult_real_positive minus_mult_commute neg_0_less_iff_less of_real_minus minus_minus)
qed (auto simp: arg_zero)

lemma arg_div_real_positive [simp]:
  assumes "k > 0"
  shows "arg (z / cor k) = arg z"
proof(cases "z = 0")
  case True
  thus ?thesis
    by auto
next
  case False
  thus ?thesis
    using assms
    using arg_mult_real_positive[of "1/k" z]
    by auto
qed

lemma arg_div_real_negative [simp]:
  assumes "k < 0"
  shows "arg (z / cor k) = arg (-z)"
proof(cases "z = 0")
  case True
  thus ?thesis
    by auto
next
  case False
  thus ?thesis
    using assms
    using arg_mult_real_negative[of "1/k" z]
    by auto
qed

lemma arg_mult_eq:
  assumes "z * z1 ≠ 0" and "z * z2 ≠ 0"
  assumes "arg (z * z1) = arg (z * z2)"
  shows "arg z1 = arg z2"
  by (metis (no_types, lifting) arg_cis assms canon_ang_arg cis_arg mult_eq_0_iff nonzero_mult_div_cancel_left sgn_divide)

text ‹Argument of conjugate›

lemma arg_cnj_pi:
  assumes "arg z = pi"
  shows "arg (cnj z) = pi"
  using arg_pi_iff assms by auto

lemma arg_cnj_not_pi:
  assumes "arg z ≠ pi"
  shows "arg (cnj z) = -arg z"
proof(cases "arg z = 0")
  case True
  thus ?thesis
    using eq_cnj_iff_real[of z] is_real_arg1[of z] by force
next
  case False
  have "arg (cnj z) = arg z ∨ arg(cnj z) = -arg z"
    using arg_bounded[of z] arg_bounded[of "cnj z"]
    by (smt (verit, best) arccos_cos arccos_cos2 cnj.sel(1) complex_cnj_zero_iff complex_mod_cnj cos_arg)
  moreover
  have "arg (cnj z) ≠ arg z"
    using sin_0_iff_canon[of "arg (cnj z)"] arg_bounded False assms
    by (metis complex_mod_cnj eq_cnj_iff_real is_real_arg2 rcis_cmod_arg)
  ultimately
  show ?thesis
    by auto
qed

text ‹Argument of reciprocal›

lemma arg_inv_not_pi:
  assumes "z ≠ 0" and "arg z ≠ pi"
  shows "arg (1 / z) = - arg z"
proof-
  have "1/z = cnj z / cor ((cmod z)⇧2 )"
    using ‹z ≠ 0› complex_mult_cnj_cmod[of z]
    by (auto simp add:field_simps)
  thus ?thesis
    using arg_div_real_positive[of "(cmod z)⇧2" "cnj z"] ‹z ≠ 0›
    using arg_cnj_not_pi[of z] ‹arg z ≠ pi›
    by auto
qed

lemma arg_inv_pi:
  assumes "z ≠ 0" and "arg z = pi"
  shows "arg (1 / z) = pi"
proof-
  have "1/z = cnj z / cor ((cmod z)⇧2 )"
    using ‹z ≠ 0› complex_mult_cnj_cmod[of z]
    by (auto simp add:field_simps)
  thus ?thesis
    using arg_div_real_positive[of "(cmod z)⇧2" "cnj z"] ‹z ≠ 0›
    using arg_cnj_pi[of z] ‹arg z = pi›
    by auto
qed

lemma arg_inv_2kpi:
  assumes "z ≠ 0"
  shows "∃ k::int. arg (1 / z) = - arg z + 2*k*pi"
  using arg_inv_pi[OF assms]
  using arg_inv_not_pi[OF assms]
  by (cases "arg z = pi") (rule_tac x="1" in exI, simp, rule_tac x="0" in exI, simp)

lemma arg_inv:
  assumes "z ≠ 0"
  shows "arg (1 / z) = ⇂- arg z⇃"
  by (metis arg_inv_not_pi arg_inv_pi assms canon_ang_arg canon_ang_uminus_pi)

text ‹Argument of quotient›

lemma arg_div_2kpi:
  assumes "z1 ≠ 0" and "z2 ≠ 0"
  shows "∃ k::int. arg (z1 / z2) = arg z1 - arg z2 + 2*k*pi"
proof-
  obtain x1 where "arg (z1 * (1 / z2)) = arg z1 + arg (1 / z2) + 2 * real_of_int x1 * pi"
    using assms arg_mult_2kpi[of z1 "1/z2"]
    by auto
  moreover
  obtain x2 where "arg (1 / z2) = - arg z2 + 2 * real_of_int x2 * pi"
    using assms arg_inv_2kpi[of z2]
    by auto
  ultimately
  show ?thesis
    by (rule_tac x="x1 + x2" in exI, simp add: field_simps)
qed

lemma arg_div:
  assumes "z1 ≠ 0" and "z2 ≠ 0"
  shows "arg(z1 / z2) = ⇂arg z1 - arg z2⇃"
proof-
  obtain k::int where "arg(z1 / z2) = arg z1 - arg z2 + 2*k*pi"
    using arg_div_2kpi[of z1 z2]
    using assms
    by auto
  hence "canon_ang(arg(z1 / z2)) = canon_ang(arg z1 - arg z2)"
    using canon_ang_eq
    by(simp add:field_simps)
  thus ?thesis
    using canon_ang_arg[of "z1/z2"]
    by auto
qed

text ‹Argument of opposite›

lemma arg_uminus:
  assumes "z ≠ 0"
  shows "arg (-z) = ⇂arg z + pi⇃"
  using assms
  using arg_mult[of "-1" z]
  using arg_complex_of_real_negative[of "-1"]
  by (auto simp add: field_simps)

lemma arg_uminus_opposite_sign:
  assumes "z ≠ 0"
  shows "arg z > 0 ⟷ ¬ arg (-z) > 0"
proof (cases "arg z = 0")
  case True
  thus ?thesis
    using assms
    by (simp add: arg_uminus)
next
  case False
  show ?thesis
  proof (cases "arg z > 0")
    case True
    thus ?thesis
      using assms
      using arg_bounded[of z]
      using canon_ang_plus_pi1[of "arg z"]
      by (simp add: arg_uminus)
  next
    case False
    thus ?thesis
      using ‹arg z ≠ 0›
      using assms
      using arg_bounded[of z]
      using canon_ang_plus_pi2[of "arg z"]
      by (simp add: arg_uminus)
  qed
qed

text ‹Sign of argument is the same as the sign of the Imaginary part›

lemma arg_Im_sgn:
  assumes "¬ is_real z"
  shows "sgn (arg z) = sgn (Im z)"
proof-
  have "z ≠ 0"
    using assms
    by auto
  then obtain r φ where polar: "z = cor r * cis φ" "φ = arg z" "r > 0"
    by (smt cmod_cis mult_eq_0_iff norm_ge_zero of_real_0)
  hence "Im z = r * sin φ"
    by (metis Im_mult_real Re_complex_of_real cis.simps(2) Im_complex_of_real)
  hence  "Im z > 0 ⟷ sin φ > 0" "Im z < 0 ⟷ sin φ < 0"
    using ‹r > 0›
    using mult_pos_pos mult_nonneg_nonneg zero_less_mult_pos mult_less_cancel_left
    by smt+
  moreover
  have "φ ≠ pi" "φ ≠ 0"
    using ‹¬ is_real z› polar cis_pi
    by force+
  hence "sin φ > 0 ⟷ φ > 0" "φ < 0 ⟷ sin φ < 0"
    using ‹φ = arg z› ‹φ ≠ 0› ‹φ ≠ pi›
    using arg_bounded[of z]
    by (smt sin_gt_zero sin_le_zero sin_pi_minus sin_0_iff_canon sin_ge_zero)+
  ultimately
  show ?thesis
    using ‹φ = arg z›
    by auto
qed


subsubsection ‹Complex square root›

definition
  "ccsqrt z = rcis (sqrt (cmod z)) (arg z / 2)"

lemma square_ccsqrt [simp]:
  shows "(ccsqrt x)⇧2 = x"
  unfolding ccsqrt_def
  by (subst DeMoivre2) (simp add: rcis_cmod_arg)

lemma ex_complex_sqrt:
  shows "∃ s::complex. s*s = z"
  unfolding power2_eq_square[symmetric]
  by (rule_tac x="csqrt z" in exI) simp

lemma ccsqrt:
  assumes "s * s = z"
  shows "s = ccsqrt z ∨ s = -ccsqrt z"
proof (cases "s = 0")
  case True
  thus ?thesis
    using assms
    unfolding ccsqrt_def
    by simp
next
  case False
  then obtain k::int where "cmod s * cmod s = cmod z" "2 * arg s - arg z = 2*k*pi"
    using assms
    using rcis_cmod_arg[of z] rcis_cmod_arg[of s]
    using arg_mult[of s s]
    using canon_ang(3)[of "2*arg s"]
    by (auto simp add: norm_mult arg_mult)
  have *: "sqrt (cmod z) = cmod s"
    using ‹cmod s * cmod s = cmod z›
    by (smt norm_not_less_zero real_sqrt_abs2)

  have **: "arg z / 2 = arg s - k*pi"
    using ‹2 * arg s - arg z = 2*k*pi›
    by simp

  have "cis (arg s - k*pi) = cis (arg s) ∨ cis (arg s - k*pi) = -cis (arg s)"
  proof (cases "even k")
    case True
    hence "cis (arg s - k*pi) = cis (arg s)"
      by (simp add: cis_def complex.corec cos_diff sin_diff)
    thus ?thesis
      by simp
  next
    case False
    hence "cis (arg s - k*pi) = -cis (arg s)"
      by (simp add: cis_def complex.corec Complex_eq cos_diff sin_diff)
    thus ?thesis
      by simp
  qed
  thus ?thesis
  proof
    assume ***: "cis (arg s - k * pi) = cis (arg s)"
    hence "s = ccsqrt z"
      using rcis_cmod_arg[of s]
      unfolding ccsqrt_def rcis_def
      by (subst *, subst **, subst ***, simp)
    thus ?thesis
      by simp
  next
    assume ***: "cis (arg s - k * pi) = -cis (arg s)"
    hence "s = - ccsqrt z"
      using rcis_cmod_arg[of s]
      unfolding ccsqrt_def rcis_def
      by (subst *, subst **, subst ***, simp)
    thus ?thesis
      by simp
  qed
qed

lemma null_ccsqrt [simp]:
  shows "ccsqrt x = 0 ⟷ x = 0"
  unfolding ccsqrt_def
  by auto

lemma ccsqrt_mult:
  shows "ccsqrt (a * b) = ccsqrt a * ccsqrt b ∨
         ccsqrt (a * b) = - ccsqrt a * ccsqrt b"
proof (cases "a = 0 ∨ b = 0")
  case True
  thus ?thesis
    by auto
next
  case False
  obtain k::int where "arg a + arg b - ⇂arg a + arg b⇃ = 2 * real_of_int k * pi"
    using canon_ang(3)[of "arg a + arg b"]
    by auto
  hence *: "⇂arg a + arg b⇃ = arg a + arg b - 2 * (real_of_int k) * pi"
    by (auto simp add: field_simps)

  have "cis (⇂arg a + arg b⇃ / 2) = cis (arg a / 2 + arg b / 2) ∨ cis (⇂arg a + arg b⇃ / 2) = - cis (arg a / 2 + arg b / 2)"
    using cos_even_kpi[of k] cos_odd_kpi[of k]
    by ((subst *)+, (subst diff_divide_distrib)+, (subst add_divide_distrib)+)
       (cases "even k", auto simp add: cis_def complex.corec Complex_eq cos_diff sin_diff)
  thus ?thesis
    using False
    unfolding ccsqrt_def
    by (smt (verit, best) arg_mult mult_minus_left mult_minus_right no_zero_divisors norm_mult rcis_def rcis_mult real_sqrt_mult)
qed

lemma csqrt_real:
  assumes "is_real x"
  shows "(Re x ≥ 0 ∧ ccsqrt x = cor (sqrt (Re x))) ∨
         (Re x < 0 ∧ ccsqrt x = 𝗂 * cor (sqrt (- (Re x))))"
proof (cases "x = 0")
  case True
  thus ?thesis
    by auto
next
  case False
  show ?thesis
  proof (cases "Re x > 0")
    case True
    hence "arg x = 0"
      using ‹is_real x›
      by (metis arg_complex_of_real_positive complex_of_real_Re)
    thus ?thesis
      using ‹Re x > 0› ‹is_real x›
      unfolding ccsqrt_def
      by (simp add: cmod_eq_Re)
  next
    case False
    hence "Re x < 0"
      using ‹x ≠ 0› ‹is_real x›
      using complex_eq_if_Re_eq by auto
    hence "arg x = pi"
      using ‹is_real x›
      by (metis arg_complex_of_real_negative complex_of_real_Re)
    thus ?thesis
      using ‹Re x < 0› ‹is_real x›
      unfolding ccsqrt_def rcis_def
      by (simp add: cis_def complex.corec Complex_eq cmod_eq_Re)
  qed
qed


text ‹Rotation of complex vector to x-axis.›

lemma is_real_rot_to_x_axis:
  assumes "z ≠ 0"
  shows "is_real (cis (-arg z) * z)"
proof (cases "arg z = pi")
  case True
  thus ?thesis
    using is_real_arg1[of z]
    by auto
next
  case False
  hence "⇂- arg z⇃ = - arg z"
    using canon_ang_eqI[of "- arg z" "-arg z"]
    using arg_bounded[of z]
    by (auto simp add: field_simps)
  hence "arg (cis (- (arg z)) * z) = 0"
    using arg_mult[of "cis (- (arg z))" z] ‹z ≠ 0›
    using arg_cis[of "- arg z"]
    by simp
  thus ?thesis
    using is_real_arg1[of "cis (- arg z) * z"]
    by auto
qed

lemma positive_rot_to_x_axis:
  assumes "z ≠ 0"
  shows "Re (cis (-arg z) * z) > 0"
  using assms
  by (smt Re_complex_of_real cis_rcis_eq mult_cancel_right1 rcis_cmod_arg rcis_mult rcis_zero_arg zero_less_norm_iff)

text ‹Inequalities involving @{term cmod}.›

lemma cmod_1_plus_mult_le:
  shows "cmod (1 + z*w) ≤ sqrt((1 + (cmod z)⇧2) * (1 + (cmod w)⇧2))"
proof-
  have "Re ((1+z*w)*(1+cnj z*cnj w)) ≤ Re (1+z*cnj z)* Re (1+w*cnj w)"
  proof-
    have "Re ((w - cnj z)*cnj(w - cnj z)) ≥ 0"
      by (subst complex_mult_cnj_cmod) (simp add: power2_eq_square)
    hence "Re (z*w + cnj z * cnj w) ≤ Re (w*cnj w) + Re(z*cnj z)"
      by (simp add: field_simps)
    thus ?thesis
      by (simp add: field_simps)
  qed
  hence "(cmod (1 + z * w))⇧2 ≤ (1 + (cmod z)⇧2) * (1 + (cmod w)⇧2)"
    by (subst cmod_square)+ simp
  thus ?thesis
    by (metis abs_norm_cancel real_sqrt_abs real_sqrt_le_iff)
qed

lemma cmod_diff_ge: 
  shows "cmod (b - c) ≥ sqrt (1 + (cmod b)⇧2) - sqrt (1 + (cmod c)⇧2)"
proof-
  have "(cmod (b - c))⇧2 + (1/2*Im(b*cnj c - c*cnj b))⇧2 ≥ 0"
    by simp
  hence "(cmod (b - c))⇧2 ≥ - (1/2*Im(b*cnj c - c*cnj b))⇧2"
    by simp
  hence "(cmod (b - c))⇧2 ≥ (1/2*Re(b*cnj c + c*cnj b))⇧2 - Re(b*cnj b*c*cnj c) "
    by (auto simp add: power2_eq_square field_simps)
  hence "Re ((b - c)*(cnj b - cnj c)) ≥ (1/2*Re(b*cnj c + c*cnj b))⇧2 - Re(b*cnj b*c*cnj c)"
    by (subst (asm) cmod_square) simp
  moreover
  have "(1 + (cmod b)⇧2) * (1 + (cmod c)⇧2) = 1 + Re(b*cnj b) + Re(c*cnj c) + Re(b*cnj b*c*cnj c)"
    by (subst cmod_square)+ (simp add: field_simps power2_eq_square)
  moreover
  have "(1 + Re (scalprod b c))⇧2 = 1 + 2*Re(scalprod b c) + ((Re (scalprod b c))⇧2)"
    by (subst power2_sum) simp
  hence "(1 + Re (scalprod b c))⇧2 = 1 + Re(b*cnj c + c*cnj b) + (1/2 * Re (b*cnj c + c*cnj b))⇧2"
    by simp
  ultimately
  have "(1 + (cmod b)⇧2) * (1 + (cmod c)⇧2) ≥ (1 + Re (scalprod b c))⇧2"
    by (simp add: field_simps)
  moreover
  have "sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2)) ≥ 0"
    by (metis one_power2 real_sqrt_sum_squares_mult_ge_zero)
  ultimately
  have "sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2)) ≥ 1 + Re (scalprod b c)"
    by (metis power2_le_imp_le real_sqrt_ge_0_iff real_sqrt_pow2_iff)
  hence "Re ((b - c) * (cnj b - cnj c)) ≥ 1 + Re (c*cnj c) + 1 + Re (b*cnj b) - 2*sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2))"
    by (simp add: field_simps)
  hence *: "(cmod (b - c))⇧2 ≥ (sqrt (1 + (cmod b)⇧2) - sqrt (1 + (cmod c)⇧2))⇧2"
    apply (subst cmod_square)+
    apply (subst (asm) cmod_square)+
    apply (subst power2_diff)
    apply (subst real_sqrt_pow2, simp)
    apply (subst real_sqrt_pow2, simp)
    apply (simp add: real_sqrt_mult)
    done
  thus ?thesis
  proof (cases "sqrt (1 + (cmod b)⇧2) - sqrt (1 + (cmod c)⇧2) > 0")
    case True
    thus ?thesis
      using power2_le_imp_le[OF *]
      by simp
  next
    case False
    hence "0 ≥ sqrt (1 + (cmod b)⇧2) - sqrt (1 + (cmod c)⇧2)"
      by (metis less_eq_real_def linorder_neqE_linordered_idom)
    moreover
    have "cmod (b - c) ≥ 0"
      by simp
    ultimately
    show ?thesis
      by (metis add_increasing monoid_add_class.add.right_neutral)
  qed
qed

lemma cmod_diff_le:
  shows "cmod (b - c) ≤ sqrt (1 + (cmod b)⇧2) + sqrt (1 + (cmod c)⇧2)"
proof-
  have "(cmod (b + c))⇧2 + (1/2*Im(b*cnj c - c*cnj b))⇧2 ≥ 0"
    by simp
  hence "(cmod (b + c))⇧2 ≥ - (1/2*Im(b*cnj c - c*cnj b))⇧2"
    by simp
  hence "(cmod (b + c))⇧2 ≥ (1/2*Re(b*cnj c + c*cnj b))⇧2 - Re(b*cnj b*c*cnj c) "
    by (auto simp add: power2_eq_square field_simps)
  hence "Re ((b + c)*(cnj b + cnj c)) ≥ (1/2*Re(b*cnj c + c*cnj b))⇧2 - Re(b*cnj b*c*cnj c)"
    by (subst (asm) cmod_square) simp
  moreover
  have "(1 + (cmod b)⇧2) * (1 + (cmod c)⇧2) = 1 + Re(b*cnj b) + Re(c*cnj c) + Re(b*cnj b*c*cnj c)"
    by (subst cmod_square)+ (simp add: field_simps power2_eq_square)
  moreover
  have ++: "2*Re(scalprod b c) = Re(b*cnj c + c*cnj b)"
    by simp
  have "(1 - Re (scalprod b c))⇧2 = 1 - 2*Re(scalprod b c) + ((Re (scalprod b c))⇧2)"
    by (subst power2_diff) simp
  hence "(1 - Re (scalprod b c))⇧2 = 1 - Re(b*cnj c + c*cnj b) + (1/2 * Re (b*cnj c + c*cnj b))⇧2"
    by (subst ++[symmetric]) simp
  ultimately
  have "(1 + (cmod b)⇧2) * (1 + (cmod c)⇧2) ≥ (1 - Re (scalprod b c))⇧2"
    by (simp add: field_simps)
  moreover
  have "sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2)) ≥ 0"
    by (metis one_power2 real_sqrt_sum_squares_mult_ge_zero)
  ultimately
  have "sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2)) ≥ 1 - Re (scalprod b c)"
    by (metis power2_le_imp_le real_sqrt_ge_0_iff real_sqrt_pow2_iff)
  hence "Re ((b - c) * (cnj b - cnj c)) ≤ 1 + Re (c*cnj c) + 1 + Re (b*cnj b) + 2*sqrt((1 + (cmod b)⇧2) * (1 + (cmod c)⇧2))"
    by (simp add: field_simps)
  hence *: "(cmod (b - c))⇧2 ≤ (sqrt (1 + (cmod b)⇧2) + sqrt (1 + (cmod c)⇧2))⇧2"
    apply (subst cmod_square)+
    apply (subst (asm) cmod_square)+
    apply (subst power2_sum)
    apply (subst real_sqrt_pow2, simp)
    apply (subst real_sqrt_pow2, simp)
    apply (simp add: real_sqrt_mult)
    done
  thus ?thesis
    using power2_le_imp_le[OF *]
    by simp
qed


text ‹Definition of Euclidean distance between two complex numbers.›

definition cdist where
  [simp]: "cdist z1 z2 ≡ cmod (z2 - z1)"

text ‹Misc. properties of complex numbers.›

lemma ex_complex_to_complex [simp]:
  fixes z1 z2 :: complex
  assumes "z1 ≠ 0" and "z2 ≠ 0"
  shows "∃k. k ≠ 0 ∧ z2 = k * z1"
  using assms
  by (rule_tac x="z2/z1" in exI) simp

lemma ex_complex_to_one [simp]:
  fixes z::complex
  assumes "z ≠ 0"
  shows "∃k. k ≠ 0 ∧ k * z = 1"
  using assms
  by (rule_tac x="1/z" in exI) simp

lemma ex_complex_to_complex2 [simp]:
  fixes z::complex
  shows "∃k. k ≠ 0 ∧ k * z = z"
  by (rule_tac x="1" in exI) simp

lemma complex_sqrt_1:
  fixes z::complex
  assumes "z ≠ 0"
  shows "z = 1 / z ⟷ z = 1 ∨ z = -1"
  using assms
  using nonzero_eq_divide_eq square_eq_iff
  by fastforce

end